$\forall$$A$:MsgA. AtomFree(ds($A$)) $\Rightarrow$ AtomFree(Type;$A$.state)